Nuprl Lemma : cmconfig?_wf
11,40
postcript
pdf
x
:chain_master(). cmconfig?(
x
)
latex
Definitions
x
,
y
,
z
.
t
(
x
;
y
;
z
)
,
x
.
t
(
x
)
,
cmconfig?(
x
)
,
t
T
,
x
:
A
.
B
(
x
)
,
x
(
s1
,
s2
,
s3
)
,
x
(
s
)
Lemmas
chain
master
wf
,
nat
wf
,
bfalse
wf
,
Id
wf
,
btrue
wf
,
bool
wf
,
chain
master
ind
wf
origin
x:chain_master(). cmconfig?(x) 
x:chain_master(). cmconfig?(x) 
x,y,z. t(x;y;z)x. t(x) Tx:A. B(x)